Problem:
 active(c()) -> mark(f(g(c())))
 active(f(g(X))) -> mark(g(X))
 proper(c()) -> ok(c())
 proper(f(X)) -> f(proper(X))
 proper(g(X)) -> g(proper(X))
 f(ok(X)) -> ok(f(X))
 g(ok(X)) -> ok(g(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 Bounds Processor:
  bound: 6
  enrichment: match
  automaton:
   final states: {8,7,6,5,4}
   transitions:
    f3(137) -> 138*
    f3(119) -> 120*
    ok2(111) -> 112*
    ok3(131) -> 132*
    ok3(138) -> 139*
    ok3(135) -> 136*
    g3(122) -> 123*
    g3(130) -> 131*
    c3() -> 135*
    active3(149) -> 150*
    ok4(144) -> 145*
    ok4(201) -> 202*
    ok4(163) -> 164*
    g4(156) -> 157*
    g4(143) -> 144*
    f4(162) -> 163*
    active0(2) -> 4*
    active0(1) -> 4*
    active0(3) -> 4*
    mark4(157) -> 158*
    c0() -> 1*
    top4(169) -> 170*
    mark0(2) -> 2*
    mark0(1) -> 2*
    mark0(3) -> 2*
    active4(173) -> 174*
    f0(2) -> 6*
    f0(1) -> 6*
    f0(3) -> 6*
    proper4(168) -> 169*
    g0(2) -> 7*
    g0(1) -> 7*
    g0(3) -> 7*
    g5(182) -> 183*
    g5(210) -> 211*
    g5(175) -> 176*
    proper0(2) -> 5*
    proper0(1) -> 5*
    proper0(3) -> 5*
    proper5(187) -> 188*
    proper5(181) -> 182*
    ok0(2) -> 3*
    ok0(1) -> 3*
    ok0(3) -> 3*
    mark5(176) -> 177*
    top0(2) -> 8*
    top0(1) -> 8*
    top0(3) -> 8*
    top5(188) -> 189*
    top1(53) -> 54*
    g6(194) -> 195*
    active1(69) -> 70*
    active1(71) -> 72*
    active1(63) -> 64*
    proper6(193) -> 194*
    proper1(55) -> 56*
    proper1(52) -> 53*
    proper1(61) -> 62*
    active5(203) -> 204*
    ok1(25) -> 26*
    ok1(17) -> 18*
    ok1(36) -> 37*
    c4() -> 201*
    g1(45) -> 46*
    g1(35) -> 36*
    g1(43) -> 44*
    g1(13) -> 14*
    ok5(211) -> 212*
    f1(27) -> 28*
    f1(24) -> 25*
    f1(14) -> 15*
    f1(33) -> 34*
    top6(217) -> 218*
    c1() -> 13*
    active6(216) -> 217*
    mark1(15) -> 16*
    top2(79) -> 80*
    active2(83) -> 84*
    proper2(102) -> 103*
    proper2(93) -> 94*
    proper2(78) -> 79*
    f2(94) -> 95*
    f2(86) -> 87*
    mark2(87) -> 88*
    g2(85) -> 86*
    g2(103) -> 104*
    c2() -> 85*
    top3(106) -> 107*
    proper3(121) -> 122*
    proper3(118) -> 119*
    proper3(105) -> 106*
    1 -> 69,55,43,27
    2 -> 63,52,35,24
    3 -> 71,61,45,33
    13 -> 102,17
    14 -> 93*
    15 -> 78*
    16 -> 70,53,4
    17 -> 83*
    18 -> 56,53,5
    26 -> 34,25,6
    28 -> 25*
    34 -> 25*
    37 -> 46,36,7
    44 -> 36*
    46 -> 36*
    54 -> 8*
    56 -> 53*
    62 -> 53*
    64 -> 53*
    70 -> 53*
    72 -> 53*
    80 -> 54,8
    84 -> 79*
    85 -> 121,111
    86 -> 118*
    87 -> 105*
    88 -> 84,79
    95 -> 79*
    104 -> 94*
    107 -> 80,54
    111 -> 130*
    112 -> 103*
    120 -> 106*
    123 -> 119*
    130 -> 156*
    131 -> 137*
    132 -> 104,94
    135 -> 143*
    136 -> 182,122
    138 -> 149*
    139 -> 95,79
    143 -> 175*
    144 -> 203,162
    145 -> 183,169,123,119
    150 -> 106*
    156 -> 181*
    157 -> 168*
    158 -> 150,106
    163 -> 173*
    164 -> 120,106
    170 -> 107,80
    174 -> 169*
    175 -> 193*
    176 -> 187*
    177 -> 174,169
    183 -> 169*
    189 -> 170,107
    195 -> 188*
    201 -> 210*
    202 -> 194*
    204 -> 188*
    211 -> 216*
    212 -> 195,188
    218 -> 189,170
  problem:
   
  Qed